Probabilistic timed automata are an extension of timed automata with discreteprobability distributions. We consider model-checking algorithms for thesubclasses of probabilistic timed automata which have one or two clocks.Firstly, we show that PCTL probabilistic model-checking problems (such asdetermining whether a set of target states can be reached with probability atleast 0.99 regardless of how nondeterminism is resolved) are PTIME-complete forone-clock probabilistic timed automata, and are EXPTIME-complete forprobabilistic timed automata with two clocks. Secondly, we show that, forone-clock probabilistic timed automata, the model-checking problem for theprobabilistic timed temporal logic PCTL is EXPTIME-complete. However, themodel-checking problem for the subclass of PCTL which does not permit bothpunctual timing bounds, which require the occurrence of an event at an exacttime point, and comparisons with probability bounds other than 0 or 1, isPTIME-complete for one-clock probabilistic timed automata.
展开▼
